00010	VAR: X,Y,Z,P,K;
00020	INF_PRED:≤,<,=;
00030	INF_OP: *;
00040	PRE_OP:1,2,S,I0,N,M,DIV,R,M0,COPY,I;
00050	EQUALITY: =;
00100	X*Y=Y*X;
00200	1*X=X;
00300	X≤X;
00400	(X≤Y∧Y≤Z)⊃X≤Z;
00500	X<Y↔(X≤Y∧¬X=Y);
00600	X≤Y∨Y≤X;
00700	X<S(X);
00800	X<Y⊃S(X)≤Y;
00900	X<2*X;
01000	S(X)≤2*X;
01100	¬(X=1)⊃X<2*X;
01200	1≤I0∧I0≤I∧I≤N∧N≤R;
01300	¬(I=I0)⊃(2*I0≤I∧COPY<M(DIV(I,2))∧M(I)≤M(DIV(I,2)));
01400	((2*I0≤K∧K≤N)⊃M(K)≤M(DIV(K,2)))∨(I=I0∧((2*S(I0)≤K∧K≤N)⊃M(K)≤M(DIV(K,2))));
01500	((1≤P∧P<I0)∨(N<P∧P≤R))⊃M(P)=M0(P);
01600	COPY=M0(I0);
01700	2*I≤N;
01800	2*I<N;
01900	M(2*I)<M(S(2*I));
02000	COPY<M(S(2*I));
02100	THEOREM:S(2*I)=I0; ;